﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\Oracles\NFMs\Oracle_NMAT_Realistic.cs
 * Description  :     A realistic oracle for non-deterministic Mealy machine for passive systems
 * Change log   :     - 10 Jan 2013: initial version
 *                    - 16 Feb 2013: removing the "possibleOutouts" and using "FindOutputTree" instead
 *                    - Nov 2013: Some bug fixed
 * To Do        :     -Change the find tree way (when an action is not enabled, return some part instead of NULL!)
 *                    -Remove public variable related to performance measuring
 ************************************************************************/
#define DebuggingMode
using System;
using System.Collections.Generic;
using AIDE.Base;
using AIDE.Utils;
using MBT.Conformance;
using MBT.Conformance.OnlineTesting;
using MBT.Conformance.TestExecution;
using MBT.Conformance.OfflineTesting;
using SMLib.Automata.Base;
using SMLib.Automata.IA;
using SMLib.Automata.MM;

namespace AIDE.Oracles.NFMs
{
	/// <summary>
	/// Here, I try to immitate a realistic Oracle which doesn'anotherRow know the machine.
	/// It has communication with SUL (in fact, an emulator of SUL)
	/// </summary>
	public class Oracle_NMAT_Realistic : IOracle_NMM
	{

		public int numberOfMQ, numberOfEQ;
		public int numberOfResetsbyNStar, numberOfExperimentForOQ, numberOfExperimentForEQ;
		public TimeSpan EqTime, OqTime, IOTime;
		DateTime startTime;
		#region Configuration Parameters
		int Debugging_Level;
		/// <summary>
		/// Use Online Testing (True: online tesing, false: edge coverage testing)
		/// </summary>
		public static bool USE_ONLINE_TESTING = true;
		///// <summary>
		///// Maximum number ?
		///// </summary>
		//public static int MAX_TrialCoEficient = 50;

		///// <summary>
		///// If after this number of trials, we found just one path, we consider the path, deterministic!
		///// </summary>
		//const int MAX_Num_Determ_Givup = 15;

		/// <summary>
		/// Number of tries to trace a path with a sequence of inputs/outputs
		/// </summary>
		public static int MAX_NUM_TRY_TO_TRACE_PATH = 5000;
		/// <summary>
		/// Minimum probability of execution of an edge in a state
		/// </summary>
		public static double MIN_PROB = 0.30;
		/// <summary>
		/// The required confidence for computation of a tree
		/// </summary>
		public static double CONF_PROB = 0.9999;
		/// <summary>
		/// Maximum number of trials where to continue the execution in case the output tree is null
		/// </summary>
		public static int MAX_NUM_TRIALS_4_NULL_TREES = 500;
		#endregion
		/// <summary>
		/// Computed number of executions for each leaf (based on MIN_PROB & CONF_PROB)
		/// </summary>
		int minNumberOfExec;
		/// <summary>
		/// The input alphabet
		/// </summary>
		Alphabet inpAlph;
		/// <summary>
		/// System under learning
		/// </summary>
		IBlackBox_MM SUL;
		/// <summary>
		/// list of inputs that are fully deterministic (periory known)
		/// </summary>
		List<ISymbol> deterInp;
		/// <summary>
		/// 
		/// </summary>
		int numberOfTries_TracePath;

		enum ModeOfWorking
		{
			PERFORMING_OUTPUT_QUERY,
			PERFORMING_EQUIVALENCE_QUERY
		}

		ModeOfWorking workingMode;
		#if UseIdealOracleInRealMode
        Oracle_NDMM_Ideal EQ_Oracle;

		
		
		#endif
		/// <summary>
		/// Oracle for non-deterministic Mealy Machine
		/// </summary>
		/// <param name="SUT">the target Mealy Machine</param>
		public Oracle_NMAT_Realistic (IBlackBox_MM SUT
#if UseIdealOracleInRealMode
, MealyMachine SUTm = null
#endif
		)
		{
			if (SUT == null)
				throw new Exception ("SUL cannot be null!");

			if (!LibSetting.IsInitialized)
				LibSetting.Init ();

			//minNumberOfExec = 1;
			//* init the configuration
			if (!int.TryParse (LibSetting.ConfOf ("AIDE.Debugging_Level"), out Debugging_Level)) {
				Debugging_Level = 3;
			}

			double.TryParse (LibSetting.ConfOf ("AIDE.NStar.CONF_PROB"), out CONF_PROB);

			double.TryParse (LibSetting.ConfOf ("AIDE.NStar.MIN_PROB"), out MIN_PROB);

			//* based on required confidence and the mininimum probability
			minNumberOfExec = (int)(Math.Log (1 - CONF_PROB) / Math.Log (1 - MIN_PROB));


			if (Debugging_Level >= 2)
				Console.WriteLine ("M=" + minNumberOfExec + " ");

			this.SUL = SUT;
			inpAlph = SUT.InputAlphabet;

			numberOfEQ = 0;
			numberOfMQ = 0;

			numberOfResetsbyNStar = 0;
			numberOfExperimentForOQ = 0;
			numberOfExperimentForEQ = 0;

			deterInp = new List<ISymbol> ();
			EqTime = TimeSpan.Zero;
			OqTime = TimeSpan.Zero;
			IOTime = TimeSpan.Zero;

#if UseIdealOracleInRealMode
            EQ_Oracle = new Oracle_NDMM_Ideal(SUTm);
#endif
		}

		/// <summary>
		/// The input alphabet (same as SUL input alphabet)
		/// </summary>
		public Alphabet inputAlphabet {
			get {
				return inpAlph;
			}
		}
		//int numberOfTrashedQuery = 0;
		#region Model Based Testing
		/// <summary>
		/// Try to trace a path of (input,output) from current position
		/// </summary>
		/// <param name="path">the path to be traced</param>
		/// <returns>true if trace was successful, false in other case</returns>
		bool TryTracingPath (List<PairOfSymbols> path)
		{
			for (int i = 0; i < path.Count; i++) {
				//DateTime temp = DateTime.Now;
				LearningLog.LogStartStepOnSUL ();
				//TODO: do not measure it for each step!
				ISymbol output = SUL.Step (path [i].Input);
				LearningLog.LogFinishStepOnSUL ();
				//IOTime += (DateTime.Now - temp);

				if (output != null && output.Equals (path [i].Output))
					continue;
				else
					return false;
			}
			return true;
		}

		/// <summary>
		/// Trace a path of (input,output) from initial node
		/// <remarks>
		/// It is similar to: public MealyMachine.Mealy_State FindNodeByPath when an automata is available
		/// (List'[PairOfStringSymbols] path, MealyMachine.Mealy_State initialNode = null)
		/// </remarks>
		/// </summary>
		/// <param name="path">the path to be traced</param>
		/// <returns>true if successful, flase if failed</returns>
		bool TracePath (List<PairOfSymbols> path)
		{
			numberOfTries_TracePath = 0;
			while (numberOfTries_TracePath < MAX_NUM_TRY_TO_TRACE_PATH) {
				//DateTime temp = DateTime.Now;

				LearningLog.LogStartSULReset ();
				SUL.Reset ();
				LearningLog.LogFinishSULReset ();

				//IOTime += (DateTime.Now - temp);

				numberOfResetsbyNStar++;
				if (workingMode == ModeOfWorking.PERFORMING_EQUIVALENCE_QUERY)
					numberOfExperimentForEQ++;
				else
					numberOfExperimentForOQ++;

				bool res = TryTracingPath (path);
				if (res) {
					//Console.WriteLine(" Step = " + numberOfTries_TracePath);
					return true;
				}
				//numberOfTrashedQuery++;
				LearningLog.CountAction ("numberOfTrashedQuery");

				numberOfTries_TracePath++;
			}
			return false;
		}

		/// <summary>
		/// try a given input sequence and keep tracking of output sequence [starting from current state]
		/// <remarks>[Convention: if we face an action that is not enabled, i.e. its output step is null, we return null]</remarks>
		/// </summary>
		/// <param name="input">the input sequence</param>
		/// <returns></returns>
		List<ISymbol> TryInputString (List<ISymbol> input)
		{
			List<ISymbol> output = new List<ISymbol> ();
			for (int i = 0; i < input.Count; i++) {
				LearningLog.LogStartStepOnSUL ();
				ISymbol o = SUL.Step (input [i]);
				LearningLog.LogFinishStepOnSUL ();

				if (o == null)
					return null;
				output.Add (o);
			}
			return output;
		}
		#endregion
		#region Output Query
		/// <summary>
		/// To inform oracle that some of inputs will never have nondeterministic outputs. This is to improve performance of
		/// oracle (to not examine the SUL several times where all inputs are deterministic)
		/// </summary>
		/// <param name="deterInp">list of input (subst of input alphabet)</param>
		public void FlagInputsAsDeterministic (List<ISymbol> deterInp)
		{
			if (this.deterInp == null)
				throw new Exception ("Null parameter is not accepted!");
			if (this.deterInp.Count != 0)
				throw new Exception ("This function can be called just one time!");
			for (int i = 0; i < deterInp.Count; i++) {
				if (!inpAlph.Contains (deterInp [i]))
					throw new Exception ("The parameter should be a subset of input alphabet!");
				this.deterInp.Add (deterInp [i]);
			}
		}
		#region =-[ Cache ]=-
		//static bool ConsiderCache = true;
		//ExecutionTrace traces = new ExecutionTrace();
		//Tree<ISymbol> InitiateTreeConsideringCache
		//    (List<PairOfSymbols> prefix, List<ISymbol> suffix, ref  List<Tree<ISymbol>.TreeNode> leaves, ref List<int> leavesExecutionNumber)
		//{
		//    ExecutionTrace.TreeNode n = traces.TracePath(prefix);
		//    if (prefix == null)
		//    {
		//        leaves = new List<Tree<ISymbol>.TreeNode>();
		//        leavesExecutionNumber = new List<int>();
		//        Tree<ISymbol> mytree = new Tree<ISymbol>();
		//        return mytree;
		//    }
		//    return null;
		//}
		#endregion
		/// <summary>
		/// Find the output tree (performing the output query in NMAT setting)
		/// <remarks>
		/// <para>If this function failed, you should increase number of trials (i.e. maximum number of trials and coef)</para>
		/// </remarks>
		/// </summary>
		/// <param name="prefix">the prefix sequence (access trace of the state)</param>
		/// <param name="suffix">the suffix to be examined</param>
		/// <returns>the computed output tree</returns>
		public Tree<ISymbol> FindOutputTree (List<PairOfSymbols> prefix, List<ISymbol> suffix)
		{
			//return EQ_Oracle.FindOutputTree(prefix, suffix);

			workingMode = ModeOfWorking.PERFORMING_OUTPUT_QUERY;

			//* DEBUG: write what we are doing...
			if (Debugging_Level >= 3) {
				Console.ForegroundColor = ConsoleColor.Blue;
				Console.WriteLine ("\n[" + ListUtil.ListToString (prefix) + "]" + ListUtil.ListToString (suffix));
				Console.ResetColor ();
			}

			//* Number of Output Queries
			numberOfMQ++;
			startTime = DateTime.Now;

			//* keep the leavses
			List<Tree<ISymbol>.TreeNode> leaves = new List<Tree<ISymbol>.TreeNode> ();
			List<int> leavesExecutionNumber = new List<int> ();
			Tree<ISymbol> mytree = new Tree<ISymbol> ();

			//if (ConsiderCache)
			//{

			//}
			//else
			//{

			//}

			int numberOfTrials = 0;

			//* check whether it can be nondeterministic or not
			//TODO: here we can optimzie. Cosider this also for leaves
			bool canBeNondeterministic = false;
			for (int i = 0; i < suffix.Count; i++) {
				if (!deterInp.Contains (suffix [i])) {
					canBeNondeterministic = true;
					break;
				}
			}

			//* if we set 'minNumberOfExec', it means that the system is fully deterministic
			if (minNumberOfExec == 1) {
				canBeNondeterministic = false;
				//Console.WriteLine("Fully deterministic!");
			}

			do {
				try {
					numberOfTrials++;
					//* the output tree is null! so, don't try more.
					if (numberOfTrials > MAX_NUM_TRIALS_4_NULL_TREES && leavesExecutionNumber.Count == 0)
						break;

					//* Try tracing the prefix
					bool success1 = TracePath (prefix);

					if (!success1) {
						Console.WriteLine ("\n****\n" + ListUtil.ListToString (prefix) + "\n****\n");
						throw new Exception ("Fail to trace a path! ");
					}

					//* If prefix was succesful, try the input string "suffix"
					List<ISymbol> output = TryInputString (suffix);

					//* If the ouputput was null, it means we explore a path in which one of actions
					//* in the suffix was not enabled!
					if (output != null) {
						Tree<ISymbol>.TreeNode mynode = mytree.Root;
						for (int ii = 0; ii < output.Count; ii++) {
							//* increament number of executed runs if it is leaves
							if (ii == output.Count - 1) {
								bool leafFound = false;
								//* increase number of executed for this node
								for (int iii = 0; iii < leaves.Count; iii++) {
									if (leaves [iii] == mynode) {
										leavesExecutionNumber [iii]++;
										leafFound = true;
										break;
									}
								}
								if (!leafFound) {
									leaves.Add (mynode);
									leavesExecutionNumber.Add (1);
								}
							}

							//* go one step in the tree
							Tree<ISymbol>.TreeNode nxtNode = mynode.ChildByEdge (output [ii]);
							if (nxtNode == null) {
								mynode = mynode.AddChild (output [ii]);
							} else {
								mynode = nxtNode;
							}
						}
					}

					//* for trace with deterministic inputs, one execution is enought!
					if (!canBeNondeterministic)
						break;


					if (leavesExecutionNumber.Count > 0) {
						int MinExec = leavesExecutionNumber [0];
						for (int ii = 1; ii < leaves.Count; ii++) {
							if (MinExec > leavesExecutionNumber [ii])
								MinExec = leavesExecutionNumber [ii];
						}
						if (MinExec > minNumberOfExec)
							break;
					} else {
						if (suffix.Count == 1)
							break;
						//* ????
						//break;
					}

				} catch (NotValidTraceException) {
					//* the trace should be skipped!
					//* we cancel our previous request for logging
					LearningLog.CancelPreviousAction ("QueryOnSUL");
				}

			} while (true);

#if DebuggingMode1
			if (!mytree.Equals(EQ_Oracle.FindOutputTree(prefix, suffix)))
				throw new Exception("Oops! Output query failed.");
#endif
			LearningLog.LogEvent ("Tree[" + prefix.ToString () + "] = " + (mytree == null ? "" : mytree.ToString ()));

			OqTime += (DateTime.Now - startTime);
			//Tree<ISymbol> myTreeR = EQ_Oracle.FindOutputTree(prefix, suffix);
			//if (!mytree.Equals(myTreeR))
			//{
			//    Console.WriteLine("WTF!");
			//}
			return mytree;
		}
		#endregion
		#region Equivalnce Query
		public static int MIN_NUM_CE = 1;

		/// <summary>
		/// See if two Mealy Machines are equal myOracle not. If they are not equal, find a counterexample to show the difference
		/// <remarks>Based on Hopcroft-Karp Algorithm [A linear algorithm for testing equivalence of finite automata]</remarks>
		/// </summary>
		/// <param name="conjucture"></param>
		/// <returns>
		/// if null, the models are the same.
		/// if not, it is a counterexample which shows the models are not the same
		/// </returns>
		public List<PairOfSymbols> EquivalenceQ (MealyMachine conjucture)
		{
			//return EQ_Oracle.EquivalenceQ(conjucture);

			workingMode = ModeOfWorking.PERFORMING_EQUIVALENCE_QUERY;

			startTime = DateTime.Now;

			numberOfEQ++;
			//* Consider the Mealy machine as an IA and try random walk on it!
			if (USE_ONLINE_TESTING) {
				//TODO this is problematic!
				MealyWrappedInIA myWrapper = new MealyWrappedInIA (SUL);
                
				InterfaceAutomaton myIolts = MealyUtils.ConvertToIOLTS (conjucture);

				SMLib.Interoperability.DOT.DotHelper_IA.WriteToDot ("TranslatedToIA.dot", myIolts);
				SMLib.Interoperability.DOT.DotHelper_MM.WriteToDot ("Original.dot", conjucture);

				//* configure the Random Walk testing
				Onlt_RandomWalk_ioco tcg
                    = new Onlt_RandomWalk_ioco (myIolts, myWrapper);
                
				//* Maximum Test Length
				Onlt_RandomWalk_ioco.MAX_TEST_LENGTH = conjucture.Size * 3;
				//* Maximum number of Tests
				Onlt_RandomWalk_ioco.MAX_NUM_TESTS = conjucture.Size * 10;
				//* Maximum number of counterexamples to be found
				Onlt_RandomWalk_ioco.MAX_NUMBER_OF_CES = 5;

				List<InterfaceAutomaton.IA_Step> counterexample = tcg.CheckConformance ();

				if (counterexample == null)
					return null;

				List<PairOfSymbols> myCounterexample = new List<PairOfSymbols> ();

				for (int i = 0; i < counterexample.Count;) {
					if (counterexample [i].StepType == InterfaceAutomaton.IA_Step.Step_Type.FUNCTION_CALL) {
						myCounterexample.Add ((PairOfSymbols)counterexample [i].Label);
						i++;
					} else if (counterexample [i].StepType == InterfaceAutomaton.IA_Step.Step_Type.ACTION) {
						ISymbol inp = ((ISymbol)counterexample [i].Label);
						i++;

						ISymbol oup;
						//***********ERROR
						if (counterexample [i] != null) {
							oup = ((ISymbol)counterexample [i].Label);
						} else {
							oup = null;
						}
						i++;
						myCounterexample.Add (new PairOfSymbols (inp, oup));
					}
				}


				return myCounterexample;
			} else {
				List<List<PairOfSymbols>> cel = new List<List<PairOfSymbols>> ();

				//* 1: Test case generator- Policy: Edge Coverag
				OTCG_EdgeCoverage<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition> ec
                    = new OTCG_EdgeCoverage<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition> (conjucture, conjucture.BranchingState);
				ec.GenerateTestCases ();
				//* 2- Test case executor
				MealyTCE te = new MealyTCE (SUL);
				te.SetModel (conjucture);


				foreach (List<MealyMachine.Mealy_Transition> tc in ec.EnumerateTestCases()) {
					List<PairOfSymbols> counterexample = null;
					try {
						counterexample = (List<PairOfSymbols>)te.FalsifyTestCase (tc);
					} catch (NotConclusiveVerdictException) {
						if (tc != null)
							LearningLog.LogEvent ("Error: Inconclusive verdict! for " + ListUtil.ListToString (tc));
						Console.WriteLine ("Error: Inconclusive verdict!");
					} catch (Exception e) {
						LearningLog.LogEvent ("Error: " + e.Message);
						Console.WriteLine ("Error: " + e.Message);
					}

					if (counterexample != null) {
						List<PairOfSymbols> ce = new List<PairOfSymbols> ();
						for (int i = 0; i < counterexample.Count; i++)
							ce.Add (new PairOfSymbols (counterexample [i].Input, counterexample [i].Output));

						Console.WriteLine ("Counterexample found! Size:" + ce.Count);
						cel.Add (ce);

						if (cel.Count >= MIN_NUM_CE)
							break;
					}
				}

				if (cel.Count == 0)
					return null;
				else {
					int maxInd = 0, maxLen = cel [0].Count;
					//Console.Write("Len = {0} ",cel[0].Count);
					for (int u = 0; u < cel.Count; u++)
						if (cel [u].Count < maxLen) {
							maxLen = cel [u].Count;
							maxInd = u;
						}
					//Console.Write("Min Len = {0} ",cel[maxInd].Count);
					return cel [maxInd];
				}
			}
		}
		#endregion
	}
}
